$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'

class Object
   def range1d?()    false end
   def range2d?()    false end
   def int?()        false end
   def point?()      false end
   def shape?()      false end
   def union?()      false end
   def graphicobj?() false end
   def prim_shape?() false end
end

#####################################################################
## GraphObj
class GraphicObj
   def graphicobj?() true end
   def self.[](*args) check_inv(self.new(*args)) end
   def initialize() abstract end
   def invariant?() abstract end
   def translate()  abstract end
   def ==(o)        abstract end
   def to_s()       abstract end
   def to_s_param() '['+self.first.to_s+','+self.last.to_s+']' end
   #def +(o) self.translate(o)end
   #def -(o) self.translate(-o)end
end

############################################################################
class Point < GraphicObj
   def point?() true  end
end

############################################################################
class Point2d < Point
   def point2d?() true  end
   def invariant?() self.first.int?() and self.last.int?() end
   
   def initialize(first,last)
      @first = first
      @last = last
   end

   def first() @first end
   def last() @last end

   def ==(p) self.equal?(p) or (p.point2d?() and self.first == p.first and self.last == p.last) end
   # Point2d x Int -> Point2d
   def translate(var) check_pre(var.int?); Point2d[self.first+var,self.last+var] end
   def to_s() 'Point2d'+ self.to_s_param end
end

############################################################################
class Shape < GraphicObj
   def shape?() true  end
   
   def invariant?() self.shape? or self.union? end
   
   def bounds() abstract end
   def in_shape?(val) abstract end
   def graph_equal_trans?(o) abstract end
end
############################################################################
class Union_Shape < Shape
   def union_shape?() true end
   
   def invariant?() self.union1d? or self.union2d? or self.diff2d? end
   
   def bounds() self.first.bounding_range(self.last) end
   # Union_Shape x Point -> Bool
   def in_shape?(val) check_pre((val.int? or val.point?)); self.first.in_shape?(val) or self.last.in_shape?(val) end
   # Union_Shape x Union_Shape -> Bool
   def graph_equal_trans?(o) check_pre(o.union_shape?); first.graph_equal_trans?(o.first) and last.graph_equal_trans?(o.last) end
end

############################################################################
class Prim_Shape < Shape
   def prim_shape?() true end
   
   def invariant?() self.range1d? or self.range2d? end
   
   def bounding_range(o) abstract end 
   def bounds() self end
   #def +(o) self.bounding_range(o) end
end

############################################################################
class Union1d < Union_Shape
   def union1d?() true end
   
   def invariant?() self.first.shape? and self.last.shape? end
   
   def initialize(first,last)
      @first = first
      @last = last
   end

   def first() @first end
   def last() @last end

   def ==(i) self.equal?(i) or (i.union1d? and self.first == i.first and self.last == i.last) end
   # Union1d x Int -> Union1d
   def translate(var) check_pre(var.int?); Union1d[self.first.translate(var),self.last.translate(var)] end
   def to_s() 'Union1d'+ self.to_s_param end
end

############################################################################
class Range1d < Prim_Shape
   def range1d?() true end

  def invariant?() self.first.int?() and self.last.int?() and self.first <= self.last end
   
   def initialize(first,last)
      @first = first
      @last = last
   end

   def first() @first end
   def last() @last end
   
   def ==(i) self.equal?(i) or (i.range1d? and self.first == i.first and self.last == i.last) end
   # Range1d x Int -> Range1d
   def translate(var) check_pre(var.int?); Range1d[self.first+var,self.last+var] end
   # Range1d x Range1d -> Range1d
   def bounding_range(val) check_pre(val.range1d?); Range1d[(self.first.min(val.first)),(self.last.max(val.last)) ] end
   def +(v) self.bounding_range(v) end
   # Range1d x Int -> Bool
   def in_shape?(val) check_pre(val.int?); (first..last).include?(val) end
   # Range1d x Range1d -> Bool
   def graph_equal_trans?(o) check_pre(o.range1d?); self.translate(o.bounds().first - self.bounds().first) == o end
   def to_s() 'Range1d'+ self.to_s_param end
end

############################################################################
class Range2d < Prim_Shape
   def range2d?() true end

   def invariant?() self.first.range1d?() and self.last.range1d?() end
   
   def initialize(first,last)
      @first = first
      @last = last
   end

   def first() @first end
   def last() @last end

   def ==(i) self.equal?(i) or (i.range2d? and self.first == i.first and self.last == i.last) end
   # Range2d x Int -> Range2d
   def translate(var) check_pre(var.int?); Range2d[self.first.translate(var),self.last.translate(var)] end
   # Range2d x Range2d -> Range2d
   def bounding_range(val) check_pre(val.range2d?); Range2d[self.first.bounding_range(val.first),self.last.bounding_range(val.last)] end
   # Range2d x Range2d -> Bool
   def in_shape?(val) check_pre(val.point2d?); first.in_shape?(val.first) and last.in_shape?(val.last) end
   # Range2d x Range2d -> Union2d
   def +(o) check_pre(o.range2d?); Union2d[self,o] end
   # Range2d x Range2d -> Bool
   def graph_equal_trans?(o) check_pre(o.range2d?); first.graph_equal_trans?(o.first) and last.graph_equal_trans?(o.last) end
   def to_s() 'Range2d'+ self.to_s_param end
end

############################################################################
class Union2d < Union_Shape
   def union2d?() true end
   
   def invariant?() self.first.shape? and self.last.shape? end
   
   def initialize(first,last)
      @first = first
      @last = last
   end

   def first() @first end
   def last() @last end

   def ==(i) self.equal?(i) or (i.union2d? and self.first == i.first and self.last == i.last) end
   # Union2d x Int -> Union2d
   def translate(var) check_pre(var.int?); Union2d[self.first.translate(var),self.last.translate(var)] end
   # Uniond2d x Range2d -> Diff2d
   def -(o) check_pre(o.range2d?); Diff2d[self,o] end
   def to_s() 'Union2d'+ self.to_s_param end
end

############################################################################
class Diff2d < Union2d
   def diff2d?() true end
   def to_s() 'Diff2d'+ self.to_s_param end
end
 
############################################################################ EOS
